Search results for "formal specification"

A syntax controlled generator of formal language processors

1963

Formal Modeling and Discrete-Time Analysis of BPEL Web Services

2008

International audience; Web services are increasingly used for building enterprise information systems according to the Service Oriented Architecture (SOA) paradigm. We propose in this paper a tool-equipped methodology allowing the formal modeling and analysis of Web services described in the BPEL language. The discrete-time transition systems modeling the behavior of BPEL descriptions are obtained by an exhaustive simulation based on a formalization of BPEL semantics using the Algebra of Timed Processes (ATP). These models are then analyzed by model checking value-based temporal logic properties using the CADP toolbox. The approach is illustrated with the design of a Web service for GPS na…

Model-based specification and validation of the dual-mode adaptive MAC protocol

2018

Wireless sensor and actuator networks (WSANs) rely on MAC protocols to coordinate access to the wireless medium access and for managing the radio unit on each device. The dual-mode adaptive MAC (DMAMAC) protocol is a recently proposed protocol designed to reduce the energy consumption of the radio communication in WSANs. The DMAMAC protocol targets the industrial WSANs used for real-time process control. At its core, DMAMAC exploits the distinction between transient and steady of the controlled plant process to dynamically adapt the MAC superframe structure and thereby conserve energy. The switch between steady and transient mode of operation is a safety-critical part of the protocol. The c…

Tool Support for Model Driven Development of Pervasive Systems

2007

This work presents the PervML Generative Tool (PervGT) that supports a model driven method for the development of pervasive services in ubiquitous environments. The tool, which is based on the Eclipse platform, provides facilities for the graphical description of pervasive systems using PervML, a UML-like modeling language. Once the pervasive system is specified, the PervML model is used as input to a transformation engine that generates source code and other implementation assets. This generated code extends an OSGi-based framework in order to build the final pervasive applications

Supporting Agile Development by Facilitating Natural User Interaction with Executable Formal Specifications

2011

Agile development benefits from fast feedback from various stakeholders. If implemented in a suitable way, formal methods can enhance the agile development process. With an executable formal specification, it is possible to analyse and simulate the behaviour of the target system before it is being built. However, for the users' and developers' natural participation in the development process, it is necessary to use a real end-user interface and bind it to the execution environment being used in the simulations and animations. This requires, though, that the execution model used to simulate the specification is appropriately changed to facilitate the use of these user interfaces. The authors…

Performance Measurement Framework with Formal Indicator Definitions

2011

Definition of appropriate measures of organization’s performance should be conducted in a systematic way. In this paper the performance measurement and indicators are discussed not only from the side of management models, but also from the point of view of measurement theories to find out appropriate definitions. In our work we propose a formal specification of indicators. The principles of indicator reformulation from free form indicators to formal requirements are formulated and applied in several examples from performance measures database. The formally defined indicators could be used in the proposed performance measurement framework that covers five-step indicator lifecycle.

Automatic Temporal Formatting of Multimedia Presentations Using Dynamic Petri Nets.

2009

An efficient authoring tool would provide support for automatic temporal formatting and modeling of multimedia presentations. Automatic temporal formatting is a process of converting the given presentation specifications into a required temporal format. This paper presents an algorithm that can convert a temporal layout into a dynamic petri net (DPN )w hich can represent iterative and interactive presentation components effectively. The prototype of the authoring tool extracts the temporal layout from any given SMIL file representation and uses the proposed algorithm to automatically convert it into a DPN. The DPN generated automatically at compile-time helps the run-time components in effe…

Extending a Metamodel for Formalization of Data Warehouse Requirements

2014

In performance measurement systems that are built on top of a data warehouse, the information requirements in natural language are different performance indicators that should be stored and analyzed. We use the requirement formalization metamodel to create a formal requirement repository out of information requirements in natural language. In the course of this research we tested the compatibility of the existing requirement formalization metamodel applying it to a set of over 150 requirements for the currently operating data warehouse project. As a result, we extended the formal specification of information requirements with some additional classes like themes, grouping, and requirement pr…

Verification of Well-Formed Communicating Recursive State Machines

2008

AbstractIn this paper we introduce a new (non-Turing equivalent) formal model of recursive concurrent programs called well-formed communicating recursive state machines (CRSM). CRSM extend recursive state machines (RSM) by allowing a restricted form of concurrency: a state of a module can be refined into a finite collection of modules (working in parallel) in a potentially recursive manner. Communication is only possible between the activations of modules invoked on the same fork. We study the model-checking problem of CRSM with respect to specifications expressed in a temporal logic that extends CaRet with a parallel operator (ConCaRet). We propose a decision algorithm that runs in time ex…

Electronic noses : specify or disappear

2000

Abstract When the quality control is achieved by using GC or GC/MS, the apparatus must comply with the applicable norms, but what about “electronic noses”? End users demand for formal specifications for selectivity, sensitivity, repeatability and sample throughput. The behavioural modelling of electronic olfactometers may provide specifications for these required parameters. This will allow both the measure itself, and evaluate the influence of the experimental errors on the sample classification. Users may expect to find a methodology allowing the performances of systems to be checked before any final decision and during routine use. We have demonstrated that the system sensitivity and log…